i, x:Id, T:Type, A, B:Realizer.
R-state(A  B;i)(x)?T ~ if x  dom(R-state(A;i)) R-state(A;i)(x)?T else R-state(B;i)(x)?T fi 

latex

Definitions	x:A. B(x), R-state(R;i), Top, t  T, x. t(x), x(s)
Lemmas	fpf-join-cap-sq, id-deq wf, R-state wf, fpf-trivial-subtype-top, Id wf, fpf wf, top wf, es realizer wf